COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "let.pub[let,jmc]" source
C00004 ENDMK
C⊗;
.require "let.pub[let,jmc]" source;
∂CSL Professor Carlos R. Borges↓Mathematics Department
↓University of California↓Davis, CA 95616∞

Dear Professor Borges:

	Martin Davis is one of the best known logicians in America,
and I am not qualified to evaluate his logical work.  However, I
know something of his work in areas touching computing and
artificial intelligence.

	He and Hilary Putnam wrote one of the first theorem proving
programs for predicate calculus, and the Davis-Putnam algorithm was
the benchmark in this field for a number of years.  More recently,
he has been interested in programs that check proofs of program
correctness, but I don't know what progress he has made.
A third recent contribution was in clarifying the mathematical
structure of non-monotonic reasoning.  So far he is the only
mathematical logician to take an interest in these problems,
and his recent article in %2Artificial Intelligence%1 was an
island of rigor and clarity in a sea of intuitive ideas.

	On the basis of this work and other contacts, I think Martin
Davis has many years of creative and productive work ahead of him,
and I look forward to seeing him more often if he moves to the
West Coast.

.sgn